Popup blocking, form filling, and many other feature of modern web browsers were first introduced as third-party extensions. New extensions continue to enrich browsers in unan- ticipated ways. However, powerful extensions require capabilities, such as cross-domain network access and local storage. Therefore, whether buggy or malicious, extensions can pose a security risk. Several browsers try to limit extension capabilities, but we show that many extensions are over-privileged under existing mechanisms.

We present a new model for extension security based around static security verification. Our model includes various compo- nents. First, we develop a lightweight authorization logic for specifying precise and fine-grained access control and information flow policies that govern an extension¦s privilege over browser re- sources (including fragments of the DOM, various URI schemes, and local storage). In comparison, prior extension models make use of relatively coarse policies, leading to over-privileged ex- tensions. Next, we show how to program extensions in ML and statically check them for compliance against these policies using refinement type checking. Static verification eliminates the need for costly runtime monitoring, and increases robustness since verified extensions cannot raise security exceptions. Finally, we show how to understand security policies by providing visualization tools that highlight the impact of a policy on particular web pages.

We evaluate our work by implementing and verifying 18 extensions with a diverse set of features and security policies. By compiling ML to either .NET or JavaScript, we are able to deploy our extensions in four different browsers ¦ IE, Chrome, Firefox, and C3. In so doing, we demonstrate how existing extension mechanisms can be enhanced with the benefits of our approach.